The Bernays–Schönfinkel class (also known as Bernays–Schönfinkel–Ramsey class) of formulas, named after
Paul Bernays
Paul Isaac Bernays (17 October 1888 – 18 September 1977) was a Swiss mathematician who made significant contributions to mathematical logic, axiomatic set theory, and the philosophy of mathematics. He was an assistant and close collaborator of ...
,
Moses Schönfinkel
Moses Ilyich Schönfinkel (russian: Моисей Исаевич Шейнфинкель, translit=Moisei Isai'evich Sheinfinkel; 29 September 1888 – 1942) was a logician and mathematician, known for the invention of combinatory logic.
Life
Mos ...
and
Frank P. Ramsey, is a fragment of
first-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quanti ...
formulas where
satisfiability
In mathematical logic, a formula is ''satisfiable'' if it is true under some assignment of values to its variables. For example, the formula x+3=y is satisfiable because it is true when x=3 and y=6, while the formula x+1=x is not satisfiable over ...
is
decidable.
It is the set of sentences that, when written in
prenex normal form, have an
quantifier prefix and do not contain any
function symbol
In formal logic and related branches of mathematics, a functional predicate, or function symbol, is a logical symbol that may be applied to an object term to produce another object term.
Functional predicates are also sometimes called mappings, bu ...
s.
This class of logic formulas is also sometimes referred as effectively propositional (EPR) since it can be effectively translated into
propositional logic
Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations ...
formulas by a process of grounding or instantiation.
The satisfiability problem for this class is
NEXPTIME-complete.
See also
*
Prenex normal form
Notes
References
*
*
Predicate logic
{{mathlogic-stub